T:Type, L:T List, R:({x:T| (x  L) }Realizer).
(xL. R-Feasible(R(x)))  (xL. yL. R(x) || R(y)  x = y  T)  R-Feasible(xL.R(x)) 

latex

Definitions	xL.R(x), (L), P  Q, left+right, s = t, Prop, x:AB(x), type List, P  Q, Type, x.A(x), (x,yL.P(x;y)), A || B, map(f;as), x(s), f(a), {x:A| B(x) }, (x  l), t  T, x:A. B(x), xL. P(x), R-Feasible(R), Realizer, Void, P  Q, l[i], T, P  Q, x:AB(x), #$n, a<b, True, {i..j}, , i  j < k, AB, P & Q, A, False, ||as||, x. t(x), x:A. B(x), A & B, <a,b>, SQType(T), {T}, s ~ t,
Lemmas	nat wf, l all map, R-compat-self, member wf, select member, R-compat-symmetry, l member subtype, length wf1, le wf, map select, true wf, squash wf, int seg wf, select wf, map length, l member wf, es realizer wf, map wf, list-set-type, R-feasible-Rlist, R-Feasible wf, R-compat wf